\documentclass[12pt]{report}
\usepackage[utf8x]{inputenc}

%Warning: tipa declares many non-standard macros used by utf8x to
%interpret utf8 characters but extra packages might have to be added
%(e.g. "textgreek" for Greek letters not already in tipa).
%Use coqdoc's option -p to add new packages.
\usepackage{tipa}

\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This file has been automatically generated with the command
%% coqdoc -utf8 -o informe/LenguajeTex/Tipos.tex --latex Tipos.v 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\coqlibrary{Tipos}{Library }{Tipos}

\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Require} \coqdockw{Export} \coqexternalref{}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.ZArith}{\coqdoclibrary{ZArith}}.\coqdoceol
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqdoclibrary{Matrix}.\coqdoceol
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqdoclibrary{Lenguaje}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdef{Tipos.Tipos}{Tipos}{\coqdocmodule{Tipos}} <: \coqdocmodule{ITipos}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Bool}{Bool}{\coqdocdefinition{Bool}} := \coqexternalref{bool}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Integer}{Integer}{\coqdocdefinition{Integer}} := \coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Byte}{Byte}{\coqdocdefinition{Byte}} := \coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Matrix}{Matrix}{\coqdocdefinition{Matrix}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n} := \coqdocdefinition{Matrix.Matrix} \coqdocvariable{A} (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{m}) (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{n}).\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.TRUE}{TRUE}{\coqdocdefinition{TRUE}} := \coqexternalref{true}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{true}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.FALSE}{FALSE}{\coqdocdefinition{FALSE}} := \coqexternalref{false}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{false}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.ZERO}{ZERO}{\coqdocdefinition{ZERO}} := 0\%\coqdocvar{Z}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int plus}{int\_plus}{\coqdocdefinition{int\_plus}} := \coqexternalref{Z.add}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.add}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.ONE}{ONE}{\coqdocdefinition{ONE}} := 1\%\coqdocvar{Z}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.bool not}{bool\_not}{\coqdocdefinition{bool\_not}} := \coqexternalref{negb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocdefinition{negb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.bool and}{bool\_and}{\coqdocdefinition{bool\_and}} := \coqexternalref{andb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocdefinition{andb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.bool or}{bool\_or}{\coqdocdefinition{bool\_or}} := \coqexternalref{orb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocdefinition{orb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int minus}{int\_minus}{\coqdocdefinition{int\_minus}} := \coqexternalref{Z.sub}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.sub}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int mult}{int\_mult}{\coqdocdefinition{int\_mult}} := \coqexternalref{Z.mul}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.mul}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int div}{int\_div}{\coqdocdefinition{int\_div}} := \coqexternalref{Z.div}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.div}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int modulo}{int\_modulo}{\coqdocdefinition{int\_modulo}} := \coqexternalref{Z.modulo}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.modulo}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int eq}{int\_eq}{\coqdocdefinition{int\_eq}} := \coqexternalref{Z.eqb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.eqb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int lt}{int\_lt}{\coqdocdefinition{int\_lt}} := \coqexternalref{Z.ltb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.ltb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int le}{int\_le}{\coqdocdefinition{int\_le}} := \coqexternalref{Z.leb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.leb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte gt}{byte\_gt}{\coqdocdefinition{byte\_gt}} := \coqexternalref{Z.gtb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.gtb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int gt}{int\_gt}{\coqdocdefinition{int\_gt}} := \coqexternalref{Z.gtb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.gtb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte eq}{byte\_eq}{\coqdocdefinition{byte\_eq}} := \coqexternalref{Z.eqb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.eqb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int ge}{int\_ge}{\coqdocdefinition{int\_ge}} := \coqexternalref{Z.geb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.geb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte xor}{byte\_xor}{\coqdocdefinition{byte\_xor}} := \coqexternalref{Z.lxor}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.lxor}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte shl}{byte\_shl}{\coqdocdefinition{byte\_shl}} := \coqexternalref{Z.shiftl}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.shiftl}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte shr}{byte\_shr}{\coqdocdefinition{byte\_shr}} := \coqexternalref{Z.shiftr}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.shiftr}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.matrix get}{matrix\_get}{\coqdocdefinition{matrix\_get}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n} \coqdocvar{i} \coqdocvar{j} (\coqdocvar{matr}: \coqref{Tipos.Tipos.Matrix}{\coqdocdefinition{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}) := \coqdocdefinition{Matrix.get} (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{i}) (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{j}) \coqdocvariable{matr}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.matrix set}{matrix\_set}{\coqdocdefinition{matrix\_set}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n} (\coqdocvar{matr}: \coqref{Tipos.Tipos.Matrix}{\coqdocdefinition{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}) \coqdocvar{i} \coqdocvar{j} \coqdocvar{a} := \coqdocdefinition{Matrix.set} (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{i}) (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{j}) \coqdocvariable{a} \coqdocvariable{matr}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.byte and}{byte\_and}{\coqdocdefinition{byte\_and}} := \coqexternalref{Z.land}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.land}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.matrix zero}{matrix\_zero}{\coqdocdefinition{matrix\_zero}} (\coqdocvar{A}:\coqdockw{Set}) (\coqdocvar{a}:\coqdocvariable{A}) \coqdocvar{m} \coqdocvar{n} := \coqdocdefinition{Matrix.new\_matr} \coqdocvariable{a} (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{m}) (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{n}).\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.z to integer}{z\_to\_integer}{\coqdocdefinition{z\_to\_integer}}(\coqdocvar{z}: \coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}): \coqref{Tipos.Tipos.Integer}{\coqdocdefinition{Integer}} := \coqdocvariable{z}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Tipos.Tipos.z to integer}{\coqdocdefinition{z\_to\_integer}} : \coqdocvar{Z} >-> \coqdocvar{Integer}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.bool to Bool}{bool\_to\_Bool}{\coqdocdefinition{bool\_to\_Bool}}(\coqdocvar{b}: \coqexternalref{bool}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{bool}}): \coqref{Tipos.Tipos.Bool}{\coqdocdefinition{Bool}} := \coqdocvariable{b}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Tipos.Tipos.bool to Bool}{\coqdocdefinition{bool\_to\_Bool}} : \coqdocvar{bool} >-> \coqdocvar{Bool}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.z to byte}{z\_to\_byte}{\coqdocdefinition{z\_to\_byte}} (\coqdocvar{z}:\coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}) : \coqref{Tipos.Tipos.Byte}{\coqdocdefinition{Byte}} := \coqdocvariable{z}.\coqdoceol
\coqdocnoindent
\coqdockw{Coercion} \coqref{Tipos.Tipos.z to byte}{\coqdocdefinition{z\_to\_byte}} : \coqdocvar{Z} >-> \coqdocvar{Byte}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{End} \coqref{Tipos}{\coqdocmodule{Tipos}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdef{Tipos.MyLenguaje}{MyLenguaje}{\coqdocmodule{MyLenguaje}} := \coqdocmodule{Lenguaje.Lenguaje} \coqref{Tipos}{\coqdocmodule{Tipos}}.\coqdoceol
\coqdocnoindent
\coqdockw{Export} \coqdocvar{Tipos}.\coqdoceol
\coqdocnoindent
\coqdockw{Export} \coqdocvar{MyLenguaje}.\coqdoceol
\end{coqdoccode}
\end{document}
